Идеи о том, что логический вывод можно свести к чисто механическому процессу, применяемому к формальному языку, были высказаны Готфридом Вильгельмом Лейбницем (1646—1716). Однако собственные работы Лейбница в области математической логики обладали серьезными недостатками, поэтому он запомнился скорее как человек, выдвинувший эти идеи как цели, которые должны быть достигнуты, а недействительно предпринявший результативную попытку их достичь.

Джордж Буль [149] впервые представил полную и работоспособную систему формальной логики в своей книге The Mathematical Analysis of Logic. Логика Буля была почти полностью промоделирована на основе обычной алгебры действительных чисел, и в ней в качестве основного метода логического вывода использовалась подстановка логически эквивалентных выражений. Хотя систему Буля еще нельзя было считать полной пропозициональной логикой, она оказалась настолько близкой к таковой, что другие математики сумели быстро заполнить все недостающие части. Шредер [1368] описал конъюнктивную нормальную форму, тогда как хорновская форма была введена намного позднее Альфредом Хорном [675]. Первое полное описание современной пропозициональной логики (и логики первого порядка) можно найти в книге Begriffschrift ("Система обозначения понятий") Готтлоба Фреге [496].

Первое механическое устройство для формирования логических выводов было сконструировано потомственным графом Стенхоупом (1753-1816). Машина Стен-хоупа, Demonstrator, была способна обрабатывать силлогизмы и некоторые логические выводы в теории вероятностей. Уильям Стэнли Джевонс, один из тех, кто усовершенствовал и расширил результаты Буля, сконструировал в 1869 году "логическое фортепьяно" для формирования выводов в булевой логике. Занимательная и поучительная история этих и других ранних механических устройств для формирования рассуждений описана Мартином Гарднером [519]. Первой опубликованной компьютерной программой для формирования логического вывода была разработанная Ньюэллом, Шоу и Саймоном программа Logic Theorist [1127]. Эта программа была предназначена для моделирования мыслительных процессов человека. Программа, позволяющая сформировать доказательство, была фактически спроектирована в 1954 году Мартином Дэвисом [334], но результаты работ в области создания программы Logic Theorist были опубликованы немного раньше. И программа Дэвиса от 1954 года, и программа Logic Theorist были основаны на достаточно произвольно выбранных методах, которые не оказали существенного влияния на дальнейшие работы в области автоматизированного дедуктивного вывода.